@echo off

IF [%1]==[] GOTO :NO_PARAMS


SET postfix=.java
SET unitpostfix=Test
SET outputpostfix=Output
SET jpfpostfix=.jpf
SET filename=%1

:FlagStart

:: Compiling the source codes and junit codes

:COMPILE_SECTION
cd .\projects\%filename%\src
SET testedfile=%filename%%postfix%
SET unittestname=%filename%%unitpostfix%
SET unittestfile=%unittestname%%postfix%
javac %testedfile% -d ..\bin
javac %unittestfile% -d ..\bin
cd ..\..\..

:: Part 1: Test Suite I Generation
:: Input: Java Source Code
:: Tool: user-defined/ Others
:: Output: Test Suite

:COVERAGE_GENERATION_SECTION
:: Part 2: Execution with Test Suite
:: Input: Java Source Code , Test Suite
:: Tool: Cobetura
:: Output: *.xml coverage information
cd .\tools\cobertura
call cobertura-instrument.bat --destination .\..\..\projects\%filename%\instrumented .\..\..\projects\%filename%\bin
java -cp .\cobertura.jar;..\..\tools\junit-4.10.jar;.\..\..\projects\%filename%\instrumented;.\..\..\projects\%filename%\bin -Dnet.sourceforge.datafile=.\cobertura.ser org.junit.runner.JUnitCore %unittestname%
:: Generate xml report
call cobertura-report.bat --format xml --datafile .\cobertura.ser --destination .\..\..\output\%filename%\report .\..\..\projects\%filename%\src
echo "XML Report Generated ..."
:: Generate html report
call cobertura-report.bat --format html --datafile .\cobertura.ser --destination .\..\..\output\%filename%\report .\..\..\projects\%filename%\src
echo "XML Report Generated ...."
cd .\..\..

:COVERAGE_ANALYSIS_SECTION
:: Part 3: Coverage Analyzing
:: Input: *.xml coverage information, Java Source Code
:: Tool: iset.coverageanalyzer
:: Output: *.jpf, instrumented Java source code
copy .\output\%filename%\report\coverage.xml .\tools\coverageanalyzer
copy .\projects\%filename%\src\*.java .\tools\coverageanalyzer\
cd .\tools\coverageanalyzer
java -jar CoverageAnalyzer.jar
::DEL  /F /Q *.java
DEL coverage.xml
cd .\..\..
echo "Press Enter to use the Symbolic JPF handling the jpf"

:: Part 4: JPF-Symbolic Execution 
:: Input: *.jpf, isntrumented *.java
:: Tool: Symbc-JPF
:: Output: Test Suite

:SYMBOLIC_SECTION
SET outputfile=%filename%%outputpostfix%%postfix%
SET outputjpf=%filename%%jpfpostfix%

CD tools\coverageanalyzer
COPY %outputfile% ..\jpf-symbc\%testedfile%
DEL  /F /Q *.java
COPY xml.jpf ..\jpf-symbc\%outputjpf%
CD ..\jpf-symbc
ECHO Paste main code to the source code and add your test case!
NOTEPAD %testedfile%
javac -g %testedfile% 
java -Xmx1000M -Djava.library.path=.\lib -jar ..\jpf-core\build\RunJPF.jar %outputjpf% > output.log
CD ..\..\

:SPF_OUTPUT_SECTION
CD tools\spfoutputanalyzer
COPY ..\jpf-symbc\output.log .\output.log
java -jar spfoa.jar
CD ..\..\

:MANUAL_ADD_TEST_CASES_SECTION
ECHO " Add more test cases into the JUnit codes according to the output."
ECHO " Example : "
ECHO "  You can add more test cases following this pattern :"
ECHO "	int result = sc.add(-100, 100);"
ECHO "  /*****Jabolic added test cases *******/ "
ECHO "  sc.add(-1000000,-1000000);sc.add(-1000000,-100);sc.add(0,-1000000);"
ECHO "  /****** please assert manually ******/ "
ECHO "  Assert.assertEquals(result,result ); "

NOTEPAD .\projects\%filename%\src\%unittestfile%

echo "Press Enter to continue this process!"
PAUSE

GOTO FlagStart

:NO_PARAMS
ECHO " Usage : framework.bat [project_name]"
ECHO " Framework processing terminated ..."

:EOF